COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE PREDCONST integer 1[R←500]
C00003 ENDMK
C⊗;
DECLARE PREDCONST integer 1[R←500];
DECLARE INDVAR m m0 m1 m2 n n0 n2 p p0 p1 p2 ε integer;
DECLARE INDCONST zero one two ε integer;

AXIOM integer: ∀n.(integer n);;

DECLARE INDCONST UU;

DECLARE OPCONST succ(integer)=integer[R←550];

AXIOM succ:
	∀m. integer succ m
;;

AXIOM peano:
	∀m.¬(succ m = zero)
	∀m n.(succ m = succ n ⊃ m = n)
;;

DECLARE PREDPAR P(integer);

AXIOM induction:
	P(zero) ∧ ∀n.(P(n) ⊃ P(succ n)) ⊃ ∀n.P(n)
;;

DECLARE OPCONST pred 1[R←550];
DECLARE OPCONST pred1 2;

AXIOM pred:
	∀n.(pred n = pred1(n,zero))
	∀n m.(pred1(n,m) = IF succ m = n THEN m ELSE pred1(n,succ m))
;;